R:Realizer, i:Id, k:Knd. write-restricted(R;i;k)  R-has-loc(R;i) 

latex

Definitions

Id, t  T, Knd, False, P  Q, x:A. B(x), s = t, Prop, a = b, b, Type, x:AB(x), x.A(x), P  Q, x:AB(x), P & Q, P  Q, {T}, x. t(x), es realizer ind Rrframe compseq tag def, R-has-loc(R;i), write-restricted(R;i;k), es realizer ind Rbframe compseq tag def, a = b, p  q, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, source(l), es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, left+right, P  Q, p  q, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, Unit, type List, IdLnk, State(ds), a:A fp B(a), DeclaredType(ds;x), rec(x.A(x)), Realizer

Lemmas

es realizer wf, unit wf, decl-type wf, fpf wf, decl-state wf, IdLnk wf, assert of bor, bor wf, R-has-loc wf, write-restricted wf, lsrc wf, iff transitivity, assert of band, and functionality wrt iff, band wf, eq knd wf, all functionality wrt iff, implies functionality wrt iff, assert-eq-id, assert wf, eq id wf, false wf, Knd wf, Id wf